$\forall$${\it es}$:ES, $i$, $x$:Id, $T$:Type, $I$:($T$$\rightarrow\mathbb{P}$).
\\[0ex](@$i$($x$:$T$) c$\wedge$ $\forall$$e$@$i$. ($\uparrow$first($e$)) $\Rightarrow$ $I$($x$ when $e$))
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. $I$($x$ when $e$) $\Rightarrow$ $I$(($x$ after $e$))
\\[0ex]$\Rightarrow$ @$i$ always.$I$($x$)